Our translated PAT model of this diagram is available here. We apply the PAT model checker to reason about the correctness of the stopwatch. As depicted below by the PAT assertion correct1, the value of centi-second (denoted by disp_cent) of the display should be equal to the centi-second (cent) of the inner counter when state Running is active. Unfortunately, the stopwatch does not hold the assertion. Actually, we can reach an error circumstance as specified by assertion error1, which states an unexpected behavior that the stopwatch displays value 0 for its centi-second variable although the inner variable centi-second is 3.

#define correct1 !(RunW_Running_Status == active) || disp_cent == cent;       #assert Stateflow() |= [] correct1;       #define error1 RunW_Running_Status == active && disp_cent == 0 && cent == 3;       #assert Stateflow() reaches error1;

By tracing the simulations of the above two assertions (thanks to the simulation facility of PAT), we identified the cause: the update of variables for display as the during action in state Running is problematic. In Stateflow, a during action of a state is executed when the state is already active and there is no valid outgoing transition at one simulation time step. In other words, a during action of a state will be skipped when the state becomes active and inactive in a pair of adjacent of simulation time steps. Here the stopwatch can behave in a similar way: initially, a user presses the start button (as event START), which activates state Running; and the user presses the lap button (as event LAP) at every simulation time step, which causes state Running is entered and exited alternatively and its during action is thus not executed, although state Run is active and updates the inner counter.